Code and Notes (Week 10 Wednesday)

{-# LANGUAGE DataKinds, KindSignatures, GADTs,
             StandaloneDeriving #-}
module W10 where

{-
data Answer = Yes | No deriving (Eq,Show)
 -}

-- GADT syntax:
data Answer :: * where -- Answer is a type of kind *, such that...
  Yes :: Answer        -- Yes is a constructor of type Answer
  No  :: Answer        -- No is a construcor type Answer
  deriving (Eq,Show) -- This *sometimes* works, but is not guaranteed
                     -- to be complete.
                     -- Or maybe it was added without Johannes noticing?
-- GADTs unfortunately do not support the `deriving` keyword
-- But: StandaloneDeriving allows us to write them stand-alone later

--deriving instance Eq Answer
--deriving instance Show Answer

{-
  data Sum a b = L a | R b

  ^ this is the same thing as Either

  data Either a b =
    Left a
  | Right b
 -}

-- We don't name the type arguments when we introduce the type constructor
data Sum :: * -> * -> * where
  L :: a -> Sum a b -- instead, we declare the type of each data constructor
  R :: b -> Sum a b

data Prod :: * -> * -> * where
  Pair :: a -> b -> Prod a b
  deriving Show

{- We're still doing things we can easily do without GADTs,
   but we're starting to see some places where the
   syntax diverges
 -}

{- Question: can we put arbitrary type variables
             in the types of L and R?
   Answer: Yes! That's one of the ways GADTs generalise datatypes
 -}
data Polarity = Positive | Negative | Zero
data Parity = Even | Odd

allTheThings :: [Sum Parity Polarity]
allTheThings =
  [L Even,
   L Odd,
   R Positive,
   R Negative,
   R Zero
   -- undefined -- these don't count
  ]

{- There's one striking fact about the number here:

      5 = 2 + 3

 -}
allTheOtherThings :: [Prod Parity Polarity]
allTheOtherThings =
  [Pair Even Positive,
   Pair Even Negative,
   Pair Even Zero,
   Pair Odd Positive,
   Pair Odd Negative,
   Pair Odd Zero
  ]

{- There's one striking fact about the number 6 here:

     6 = 2 * 3
 -}

{- Remember earlier in the course, we've seen:
   - plain old lists

      data [a] = [] | a:[a]

   - non-empty lists (lists that are non-empty by construction)

      data NonEmpty a = Single a | Cons a (NonEmpty a)

   The advantage of non-empty list is that we can define

      safeHead  :: NonEmpty a -> a
      safeTail  :: NonEmpty a -> [a]
                   ^^ the tail of a non-empty list isn't necessarily empty

   which are *total* functions.

  But: what if I wanted a type for:
   - lists with at least two elements?
   - a type specifically for empty lists

  GADTs + phantom types gives us a way to define *all* of these types
   in one go.

  First ingredient: type-level numbers.
   Numbers that only exist at compile time in the type system,
   and are not used at all at runtime.
 -}

data Nat = Z | S Nat
{- Z     represents 0
   S(n)  represents n+1

   S(S(Z)) represents 2

   Remember: we enabled DataKinds,
     which means that every datatype declaration
     also simultatenously defines a kind.

   Nat is a *kind*
   which is inhabited by countable many types:

       Z       :: Nat
       S Z     :: Nat
       S(S(Z)) :: Nat

   ^ The type Z is not inhabited by any values,
     so we can only use it as a phantom type.

     But we can use it to enforce requirements on length.
 -}

-- Sized lists: lists where the size of the list is encoded
-- in its type by a type-level natural number
data Vec :: Nat -> * -> * where
  Nil  :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

deriving instance Eq a => Eq(Vec n a)
deriving instance Show a => Show(Vec n a)

-- This completely subsumes NonEmpty lists from before

safeHead :: Vec (S n) a -> a
safeHead (Cons x xs) = x
-- Even though we haven't written a case for Nil,
-- this pattern matching is nonetheless exhaustive.
-- [a] a list of arbitrary length
-- We know that the argument is a list of length
   -- n+1 for some n
safeTail :: Vec (S n) a -> Vec n a
safeTail (Cons x xs) = xs

{- Not only can we do type-safe head and tail
   We can do type-safe head-of-tail
 -}
sndElement :: Vec (S (S n)) a -> a
sndElement = safeHead . safeTail
--sndElement(Cons _ (Cons y _)) = y

{- Let's define map!
 -}
mapV :: (a -> b) -> Vec n a -> Vec n b
mapV f Nil = Nil
mapV f (Cons x xs) = Cons (f x) (mapV f xs)

{- zipV that enforces that both lists have the same length
 -}
zipV :: Vec n a -> Vec n b -> Vec n (a,b)
zipV Nil Nil = Nil
zipV (Cons x xs) (Cons y ys) = Cons (x,y) (zipV xs ys)


safeLast :: Vec (S n) a -> a
safeLast (Cons x Nil) = x
safeLast (Cons x xs) = safeLast xs

-- What's something that's difficult to do?
-- Let's (not) define append (aka ++)
-- We'd like to have this type signature:
--append :: Vec n a -> Vec m a -> Vec (n+m) a
-- but we don't have a definition of + for type-level numbers
-- you can make one, but it requires even more extensions

-- What's something you can't do?
-- We can't write this function:
--  filterV :: (a -> Bool) -> Vec n a -> Vec ??? a
-- We have no way of knowing statically how many
-- elements the return value has.
-- Therefore, filterV has to return a non-sized list:
--  filterV :: (a -> Bool) -> Vec n a -> [a]

{-  Previously, we would have proved by equational reasoning that

      length(map f xs) = length xs

    Now, we don't have to! The type of `mapV` already enforces  that
    the length of the argument and return vector are the same,
    because they're referring to the same number n

 -}


{- A type-safe RPN calculator
   *without* zero-padding
 -}

-- Intuitively: the type-level number means
--   the number of elements that must exist on the stack
--   in order to run this computation successfully
data RPN :: Nat -> * where
  Add      :: RPN (S n) -> RPN (S(S n))
  Enter    :: Int -> RPN (S n) -> RPN n
  Done     :: RPN (S Z) -- Done expects a 1-element stack
                        -- because the point of the calculation
                        -- is to compute a number
  AllClear :: RPN Z -> RPN n

calc' :: RPN n -> Vec n Int -> Int
calc' (Add i) (Cons x (Cons y s)) =
  calc' i (Cons (x+y) s)
calc' (Enter x i) s =
  calc' i (Cons x s)
calc' Done (Cons x _) = x
calc' (AllClear i) s =
  calc' i Nil

calc :: RPN Z -> Int
calc i = calc' i Nil

{-
  Enter 2 $ AllClear $ Enter 3 $ Enter 4 $ Add $ Done
                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                        this calculation has type RPN Z
 -}

{- What classes should  you take if you want to pursue functional programming?


    3141

    3161 Concepts of Programming Languages,
          the other "not a Haskell course" course
          more focussed on foundations as opposed to programming
    to a lesser extent
    4161
     ^ more focussed on formal verification
        (proving programs correct)
       in a language that shares a lot of DNA with Haskell
 -}